Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: Add String.length_join and List.length_join #770

Merged
merged 2 commits into from
May 3, 2024
Merged

feat: Add String.length_join and List.length_join #770

merged 2 commits into from
May 3, 2024

Conversation

tjf801
Copy link
Contributor

@tjf801 tjf801 commented Apr 28, 2024

No description provided.

@tjf801
Copy link
Contributor Author

tjf801 commented Apr 28, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Apr 28, 2024
kim-em
kim-em reviewed Apr 30, 2024
View reviewed changes
Std/Data/String/Lemmas.lean Outdated Show resolved Hide resolved
kim-em
kim-em reviewed Apr 30, 2024
View reviewed changes
Std/Data/String/Lemmas.lean Outdated Show resolved Hide resolved
@kim-em
Copy link
Collaborator

kim-em commented Apr 30, 2024

Otherwise, great, thank you!

@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Apr 30, 2024
@tjf801 @kim-em
Update Std/Data/List/Lemmas.lean
445b714 
Update Std/Data/String/Lemmas.lean

Co-Authored-By: Kim Morrison <[email protected]>
@tjf801
Copy link
Contributor Author

tjf801 commented May 1, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels May 1, 2024
@kim-em kim-em merged commit 123fb93 into leanprover-community:main May 3, 2024
1 check passed
kim-em added a commit that referenced this pull request May 3, 2024
@kim-em
Revert "Add String.length_join and List.length_join (#770)"
80cf5a1 
This reverts commit 123fb93.
@kim-em
Copy link
Collaborator

kim-em commented May 3, 2024

Oops, I merged this, but it caused master to fail. Very sorry, but would you reopen against current main, fix the problem, and then ping me?

@tjf801
Copy link
Contributor Author

tjf801 commented May 3, 2024

Yup! No problem. Seems to be that somehow Std.Data.Nat got removed through a few indirect layers of imports since the code was tested, so I just explicitly added it back into Std.Data.List.Lemmas.

@tjf801 tjf801 mentioned this pull request May 3, 2024
Open
@tjf801
Copy link
Contributor Author

tjf801 commented May 3, 2024

@semorrison opened the new PR under #779

@tjf801 tjf801 changed the title Add String.length_join and List.length_join feat: Add String.length_join and List.length_join May 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tjf801 @kim-em